Example 5.7 in [Lucas - PLILP'97]

Summary: Ex5_7_Luc97

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (Extra variables)

CS-TRS Ex5_7_Luc97 (file Ex5_7_Luc97.csr)

Functions:  dbl 0 s dbls nil cons sel indx from dbl1 01 s1 sel1 quote

Constructors:  0 s nil cons 01 s1

Variables:  X Y Z

Arities: 

ar(dbl) = 1
ar(0) = 0
ar(s) = 1
ar(dbls) = 1
ar(nil) = 0
ar(cons) = 2
ar(sel) = 2
ar(indx) = 2
ar(from) = 1
ar(dbl1) = 1
ar(01) = 0
ar(s1) = 1
ar(sel1) = 2
ar(quote) = 1

Replacement map: 

µ(dbl)={1}
µ(0)={}
µ(s)={1}
µ(dbls)={1}
µ(nil)={}
µ(cons)={}
µ(sel)={1,2}
µ(indx)={1}
µ(from)={}
µ(dbl1)={1}
µ(01)={}
µ(s1)={1}
µ(sel1)={1,2}
µ(quote)={1}

Rules:  (file Ex5_7_Luc97)  

dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
dbls(nil) -> nil
dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y))
sel(0,cons(X,Y)) -> X
sel(s(X),cons(Y,Z)) -> sel(X,Z)
indx(nil,X) -> nil
indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z))
from(X) -> cons(X,from(s(X)))
dbl1(0) -> 01
dbl1(s(X)) -> s1(s1(dbl1(X)))
sel1(0,cons(X,Y)) -> X
sel1(s(X),cons(Y,Z)) -> sel1(X,Z)
quote(0) -> 01
quote(s(X)) -> s1(quote(X))
quote(dbl(X)) -> dbl1(X)
quote(sel(X,Y)) -> sel1(X,Y)

The CS-TRS in OBJ format (file Ex5_7_Luc97.obj):

obj Ex5_7_Luc97 is
  sort S .
  op dbl : S -> S .
  op 0 : -> S .
  op s : S -> S .
  op dbls : S -> S .
  op nil : -> S .
  op cons : S S -> S [strat (0)] .
  op sel : S S -> S .
  op indx : S S -> S [strat (1 0)] .
  op from : S -> S [strat (0)] .
  op dbl1 : S -> S .
  op 01 : -> S .
  op s1 : S -> S .
  op sel1 : S S -> S .
  op quote : S -> S .
  vars X Y Z : S .
  eq dbl(0) = 0 .
  eq dbl(s(X)) = s(s(dbl(X))) .
  eq dbls(nil) = nil .
  eq dbls(cons(X,Y)) = cons(dbl(X),dbls(Y)) .
  eq sel(0,cons(X,Y)) = X .
  eq sel(s(X),cons(Y,Z)) = sel(X,Z) .
  eq indx(nil,X) = nil .
  eq indx(cons(X,Y),Z) = cons(sel(X,Z),indx(Y,Z)) .
  eq from(X) = cons(X,from(s(X))) .
  eq dbl1(0) = 01 .
  eq dbl1(s(X)) = s1(s1(dbl1(X))) .
  eq sel1(0,cons(X,Y)) = X .
  eq sel1(s(X),cons(Y,Z)) = sel1(X,Z) .
  eq quote(0) = 01 .
  eq quote(s(X)) = s1(quote(X)) .
  eq quote(dbl(X)) = dbl1(X) .
  eq quote(sel(X,Y)) = sel1(X,Y) .
endo

Negative results

1. The µ-termination of Ex5_7_Luc97 cannot be proved by using Lucas' transformation. The TRS Ex5_7_Luc97_L:

       dbl(0) -> 0
       dbl(s) -> s
       dbls(nil) -> nil
       dbls(cons) -> cons
       sel(0,cons) -> X
       sel(s,cons) -> sel(X,Z)
       indx(nil) -> nil
       indx(cons) -> cons
       from -> cons
       dbl1(0) -> 01
       dbl1(s) -> s1(s1(dbl1(X)))
       sel1(0,cons) -> X
       sel1(s,cons) -> sel1(X,Z)
       quote(0) -> 01
       quote(s) -> s1(quote(X))
       quote(dbl(X)) -> dbl1(X)
       quote(sel(X,Y)) -> sel1(X,Y)
       

   contains extra variables.